\begin{tabbing}
ma{-}sub\=\{i:l\}\+
\\[0ex]($M_{1}$; $M_{2}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(fpf{-}sub(Id; $x$.Type\{i\}; IdDeq; ($M_{1}$.1); ($M_{2}$.1))\+
\\[0ex]\& fpf{-}sub(Knd; $x$.Type\{i\}; KindDeq; (($M_{1}$.2).1); (($M_{2}$.2).1)))
\\[0ex]c$\wedge$ \=(fpf{-}sub(Id; $x$.($\mathbb{Q}\rightarrow$fpf{-}cap($M_{2}$.1;IdDeq;$x$;Void)); IdDeq; (($M_{1}$.2.2).1); (($M_{2}$.2.2).1))\+
\\[0ex]\& fpf{-}sub(Id; $a$.(State($M_{2}$.1)$\rightarrow\mathbb{B}$); IdDeq; (($M_{1}$.2.2.2).1); (($M_{2}$.2.2.2).1))
\\[0ex]\& fpf{-}sub(\=(:Knd $\times$ Id);\+
\\[0ex]${\it kx}$.(State($M_{2}$.1)$\rightarrow$Valtype(($M_{2}$.2).1;${\it kx}$.1)$\rightarrow\mathbb{Q}\rightarrow$
\\[0ex]fpf{-}cap($M_{2}$.1;IdDeq;${\it kx}$.2;Void));
\\[0ex]product{-}deq(Knd;Id;KindDeq;IdDeq);
\\[0ex](($M_{1}$.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(\=(:Knd $\times$ IdLnk);\+
\\[0ex]${\it kl}$.((${\it tg}$:Id
\\[0ex]$\times$ \=(State($M_{2}$.1)$\rightarrow$Valtype(($M_{2}$.2).1;${\it kl}$.1)$\rightarrow$\+
\\[0ex](fpf{-}cap(($M_{2}$.2).1;KindDeq;rcv(${\it kl}$.2,${\it tg}$);Void) List))) List);
\-\\[0ex]product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);
\\[0ex](($M_{1}$.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(Id; $x$.(Knd List); IdDeq; (($M_{1}$.2.2.2.2.2.2).1); (($M_{2}$.2.2.2.2.2.2).1))
\\[0ex]\& fpf{-}sub(\=(:IdLnk $\times$ Id);\+
\\[0ex]${\it ltg}$.(Knd List);
\\[0ex]product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);
\\[0ex](($M_{1}$.2.2.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(\=Knd;\+
\\[0ex]$k$.(Id List);
\\[0ex]KindDeq;
\\[0ex](($M_{1}$.2.2.2.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(\=Knd;\+
\\[0ex]$k$.(IdLnk List);
\\[0ex]KindDeq;
\\[0ex](($M_{1}$.2.2.2.2.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(\=Id;\+
\\[0ex]$x$.(Knd List);
\\[0ex]IdDeq;
\\[0ex](($M_{1}$.2.2.2.2.2.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2.2.2.2.2.2).1))
\-\\[0ex]\& fpf{-}sub(\=Id;\+
\\[0ex]$x$.FinProbSpace;
\\[0ex]IdDeq;
\\[0ex](($M_{1}$.2.2.2.2.2.2.2.2.2.2.2).1);
\\[0ex](($M_{2}$.2.2.2.2.2.2.2.2.2.2.2).1)))
\-\-\-
\end{tabbing}